Skip to content

Expand Laurel implementation, so that tests T2 (impure expressions) and T3 (dag control flow) pass as well#2

Draft
keyboardDrummer wants to merge 116 commits intomainfrom
laurelMoreStmtExpr
Draft

Expand Laurel implementation, so that tests T2 (impure expressions) and T3 (dag control flow) pass as well#2
keyboardDrummer wants to merge 116 commits intomainfrom
laurelMoreStmtExpr

Conversation

@keyboardDrummer
Copy link
Copy Markdown
Owner

@keyboardDrummer keyboardDrummer commented Dec 18, 2025

Changes

  • Update testing infrastructure so the Laurel examples that include expected diagnostics can be run from the file where they are defined in.
    • Updated Laurel tests T1 to T10 to use this
  • Add a ToFormat instance for the Laurel type to help with debugging
  • Make changes so that Laurel test T2 and T3 pass.
    • This includes simple extensions to ConcreteToAbstractTreeTranslator and LaurelToBoogieTranslator, which perform 1-1 translations.
    • The most interesting change is the addition of LiftExpressionAssignments, which attempts to lift any assignments that occur in an expression position so they are done in the innermost enclosing statement block instead.

Caveats

I think there are a lot of cases of impure expressions that aren't supported yet. It would be good to add explicit tests for those and to return not supported diagnostics in those cases. Created a GH issue to address something that's not supported: strata-org#282

Testing

  • Laurel T2 and T3 are now running and passing as well.

@keyboardDrummer keyboardDrummer changed the base branch from laurelParsing to main December 24, 2025 12:43
keyboardDrummer added a commit that referenced this pull request Feb 13, 2026
### Changes
- Add a Python script in `Tools` that enables automatically updating the
results of `#guard_msg`
- Update formatting of applications in Core. A good way to see how the
formatting has changed is to look at the updated tests in this PR.

Before:
```
while (((~Int.Lt i) n)) (some ((~Int.Sub n) i)) (some ((~Bool.And ((~Int.Le i) n)) (((~Int.Div ((~Int.Mul i) ((~Int.Sub i) #1))) #2) == sum))) {sum := ((~Int.Add sum) i)
 i := ((~Int.Add i) #1)}
```
After:
```
  while
    (~Int.Lt i n)
    (some (~Int.Sub n i))
    (some (~Bool.And (~Int.Le i n) ((~Int.Div (~Int.Mul i (~Int.Sub i #1)) #2) == sum)))
  {
    sum := (~Int.Add sum i)
    i := (~Int.Add i #1)
  }
```


Applications in expressions require fewer parenthesis are are shown in a
tree like fashion when they do not fit on a line:

Before
```
/-- info: Annotated expression:
((((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int)))) (((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string))))) (((~Prod : (arrow int (arrow string (Tup int string)))) #3) #a)) (((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string))))) (((~Prod : (arrow int (arrow string (Tup int string)))) #4) #b)) (~Nil : (List (Tup int string)))))) #0) (λ (λ (λ (((~Int.Add : (arrow int (arrow int int))) (((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int))) %2) (λ (λ %1)))) ((((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int)))) %1) #1) (λ (λ (λ (((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int))) %2) (λ (λ %1))))))))))))
```
After
```
/--
info: Annotated expression:
((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int))))
 ((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string)))))
  ((~Prod : (arrow int (arrow string (Tup int string)))) #3 #a)
  ((~Cons : (arrow (Tup int string) (arrow (List (Tup int string)) (List (Tup int string)))))
   ((~Prod : (arrow int (arrow string (Tup int string)))) #4 #b)
   (~Nil : (List (Tup int string)))))
 #0
 (λ (λ (λ ((~Int.Add : (arrow int (arrow int int)))
     ((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int))) %2 (λ (λ %1)))
     ((~List$Elim : (arrow (List (Tup int string)) (arrow int (arrow (arrow (Tup int string) (arrow (List (Tup int string)) (arrow int int))) int))))
      %1
      #1
      (λ (λ (λ ((~Tup$Elim : (arrow (Tup int string) (arrow (arrow int (arrow string int)) int)))
          %2
          (λ (λ %1))))))))))))
```

### Testing
Updated tests

---------

Co-authored-by: Andrew Wells <130512013+andrewmwells-amazon@users.noreply.github.com>
@github-actions github-actions Bot added the Git conflicts PR has merge conflicts with the base branch label Apr 21, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Git conflicts PR has merge conflicts with the base branch

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants